a:. |a| ~ a 

latex

Definitions	x:A. B(x), |i|, t  T, Unit, P  Q, P & Q, P  Q, T, P  Q, ij, AB, , i<j, b, b, True, Prop
Lemmas	neg assoced, assoced weakening, bnot wf, assert wf, lt int wf, le wf, bool wf, le int wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, assert of le int, eqtt to assert